a, b:. (a + -(a) + b) = b & (-(a) + a + b) = b 

latex

Definitions	IMonoid, t  T, IGroup, t.2, t.1, , Mon, Group{i}, AbGrp, <+>, ~, *, x f y, |g|, P & Q, x:A. B(x)
Lemmas	abgrp wf, grp inv wf, inverse wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf, grp inv assoc